00100		This conference is about proving assertions about programs, and I'd
00200	like to say a little bit about the state of this.  Saying something about the
00300	state of this reminds me of the introduction of a book by G.H. Hardy called
00400	Pure Mathematics (I'm talking about the third or fourth edition) and he
00500	remarks in the third or fourth edition that he thought that this was the
00600	first texted analysis to introduce rigorous methods in elementary calculus.
00700	He thought that if he were doing if over again he would write with a decent
00800	terseness and restraint and not so much like a missionary lecturing to
00900	cannibals.  Maybe I should do that.
01000	
01100		I'd like to mention one other thing.  The first time I gave a paper
01200	on Mathematical Theory of Computation, or Proving Assertions about Programs,
01300	was in 1961 at the Western Joint Computer Conference, as it was called then.
01400	And I was pounding the table away and advertising the subject, saying
01500	it's a mathematical disgrace that here a program is a mathematical object
01600	and yet all the mathematicians treat it like a piece of experimental
01700	apparatus.  They debug it rather than proving it, and that what we've got
01800	to do is to eliminate debugging.  And the audience started to laugh.  I didn't
01900	understand why they were laughing.  I was facing the viewgraph, no I wasn't
02000	facing the viewgraph.  I don't know where I was facing, I was facing the
02100	audience.  Anyway there was this big laugh and I looked around and I
02200	finally gave up on trying to understand what they were laughing at and
02300	went on.  Finally somebody told me later that while I was talking about this
02400	there was this bug crawling around on the viewgraph highly magnified and
02500	when I pounded the table and talked about debugging, the bug flew away.
02600	Corbato accused me of having arranged that, but I'm not really capable
02700	of anything as cleaver as that.
02800	
02900		I would like to talk a little bit about the state of affairs
03000	as it is now as compared to what it was 10 years ago.  I don't know
03100	whether this is really true or not but it seemed to me at that time
03200	there were very few people interested in proving assertions about
03300	computer programs.  In my opinion, this is, in a sense, one of the main
03400	areas of contact between mathematics and computer science and that it
03500	really does have these great practical implications, which if we can
03600	work it out, it should eventually turn out that noone will pay for a
03700	computer program unless it has been proved to be correct and this
03800	proof checked on a computer.  If we look at the situation 10 years ago,
03900	people weren't even very much interested in that problem.  There were
04000	those who thought that a Turing machine was more scientific than any
04100	other kind of computer and that the thing to do was to make computers
04200	look like Turing machines.  Well, that's a charicature of them.  There
04300	were the Markov algorithm fans.  The theory problem of trying to make a
04400	theory in which you could prove programs correct had a tendency to be
04500	confused with the artificial intelligence problem of how to make a
04600	computer program that could prove programs correct all by itself.  And
04700	in a sense one of our pieces of progress in the last 10 years has been
04800	to accept this more modest goal of having a formalism in which it is
04900	possible to prove programs correct.  Now I think we know quite a lot
05000	more about what the real problems are today.
05100	
05200		I think one other thing which has contributed to the advance of this
05300	subject and of proving assertions about programs as compared to some of the
05400	other areas that were popular then, and I guess many of them are still
05500	quite popular now, is the practical implications.  I think this is one of
05600	the areas where the practical aspects of the matter do  indeed bring out
05700	interesting theoretical problems which are valuable from even the point
05800	of view of pure mathematics.
05900	
06000		I'd like to say a little bit about how some of my ideas have
06100	changed about mathematical theory of computation, some of the things I
06200	was wrong about.  The first thing I should do is agree with the opinion
06300	which Zohar implied today which is that the lack of correspondence
06400	between the results of the CALL-BY value in LISP and in other languages
06500	and the minimal fixed point, is indeed a bug in LISP.  I don't know how
06600	to fix it but as far as I'm concerned, it's  a bug.  It's too bad that
06700	it doesn't correspond and we should make it correspond.
06800	
06900		Let's consider how far along we are towards the practical goal
07000	of being able to prove that programs are correct as a regular part of
07100	the preparation of the program for people's use.  What we would need in
07200	order to do this is to have properly formalized the programming languages
07300	that we will use, to have the programmers educated in the technique which
07400	so far does not exist of proving assertions about their programs, and
07500	to have adequate proof checkers that can check these proofs in a
07600	reasonable time.  I suppose we should also know, we would have to know
07700	quite a bit more about how to express our desires for the program in the
07800	form of formal assertions whose truth we would like to have verified.  But
07900	certainly we know how to express many of our desires of a program.  That
08000	is that they should terminate and that they should use only their own
08100	storage, and then the further matter that they should get the right
08200	answer.  We can express that in some cases, and find it a little difficult
08300	in other cases. 
08400	
08500		Progress can be regarded as a number of steps.  For example, as far
08600	as the formal definition of programming languages is concerned, there is the
08700	monumental job that the IBM Vienna group has done on formally defining
08800	PL-1 and the extension by these same methods to a formal definition to
08900	ALGOL (I'm not quite sure what the status of that is, but it seems to me
09000	it's in a similar state).  On the other hand, the Vienna definition language
09100	which is used for this purpose has not been axiomatized, in the sense that
09200	there is some proof that some set of axioms is categorical for these
09300	entities, and  a fortiori,     no PL-1 compiler  has been proved correct.
09400	Now, in terms of proving compilers correct, only toy compilers have been
09500	proved correct.  Actually, one would even have to hesitate on that and say
09600	well, it wasn't actually any compiler that was proved correct, it was
09700	a toy compiling algorithms have been proved correct.  There's the paper by
09800	me and Painter which proves correct an algorithm for compiling arithmetic
09900	expressions, and then there are the papers by Kaplan and Painter (separate
10000	papers) proving subsets of ALGOL correct in some sense.  I would say that
10200	in that respect that the paper by me and Painter is in its area on
10300	the right track in making the formalisms for the others we somehow got lost
10400	in the woods and we'll have to backtrack and find some better way of doing
10500	it, otherwise it won't work.  However, there have been some recent results
10600	namely, Whit Diffie almost has computer-checked a computer proof of this
10700	toy-compiling algorithm for arithmetic expressions.  So if you remember
10800	all those qualifications, it's almost checked and it's only the algorithm
10900	and not the compiler itself, which tells us something of where we are
11000	and as Robin Milner mentioned today, a compiler itself is in the works
11100	for being proved correct, but where the language in which this compiler
11200	is expressed is essentially its abstract syntax rather than its concrete
11300	syntax, and that I think will represent some additional progress.  As far
11400	as proving programs themselves correct, we again have toy programs have
11500	been proved correct with a kind of informal translation from the program
11600	to the statements in predicate calculus which have to be proved correct.
11700	I think that one would have to describe the translation that is prescribed
11800	in Floyd's method and the translation prescribed in Manna's methods and
11900	methods of that kind is a kind of informal mathematical translation and
12000	doesn't work directly with the text of the program.  I guess Kingsworth
12100	works with the text of the program.  As far as real programs which anyone
12200	has any interest in, proving them correct has only been done informally
12300	and I guess the one who has done the most in that area is Ralph London.
12400	I was very pleased to see in the proceedings of this conference the
12500	first step towards connecting the theory of proving programs correct with
12600	the mathematical theory that is embodied in numerical analysis.  There are
12700	some other areas which are sort of coming along, and that's the area of
12800	parallel programs.  I always thought that parallel programs, well, that's
12900	something that can wait to prove correct until they get ILLIAC IV debugged.
13000	And I figure that we could put that off for quite a while. But now
13100	it turns out that parallel programs and indeterminate programs turn out
13200	to have a kind of very large significance because if we want to consider any
13300	kind of system that has not only the computer program itself but other
13400	entities in it like people, then we can for some purposes, regard people
13500	as indeterminate programs.  I shall mention this in connection with
13600	a problem which I've been toying with for a while, which is to prove
13700	correct the McCarthy airline reservation system.  The McCarthy airline
13800	reservation system is the reservation system for the McCarthy airline
13900	and this airline has one seat.  It has a great safety record because the
14000	airplane never flies.  It has only two customers because of this
14100	disadvantage, and the two customers may at one time or another reserve
14200	the seat, if they can, or cancel the reservation.  I think we could about
14300	prove that the airline reservation system that will correctly keep track
14400	of this one seat is correct by getting a suitable formula of predicate
14500	calculus.  Of course, a customer is represented by an indeterminate
14600	program who at any moment may decide either to make a reservation or
14700	cancel a reservation, or perhaps do nothing.
14800	
14900		Now, it seems to me that proving programs correct can be
15000	regarded really as a practical matter, as part of their usage, can be
15100	regarded as only a first step towards achieving a more general goal
15200	which I would have to say goes back to Liebniz.  Liebniz wanted to
15300	mathematize reasoning and he wanted to have people do the right thing
15400	by proving that it was the right thing.  I better not say anything more
15500	about Liebniz for fear of being wrong.  But one can see that we are
15600	really very far from that, but we are a lot closer than we used to be
15700	because here's one area, namely computer programs themselves which are
15800	a kind of practical area, in which we can at least think about the
15900	problems of proving them correct and we can see that the problems that face us
16000	here are technical problems rather than problems in principle.  However,
16100	let us consider the following fantasy and that is that we would like to
16200	consider any kind of policy that, let us say the government has or a
16300	commercial organization has, and we would imagine that this policy has a
16400	kind of rationalization of which is a pseudo-proof that it is correct,
16500	or at least a pseudo-proof  that it is better than the other policies
16600	that have been considered up to that time.  And along comes some fellow
16700	sitting at his home console or we will imagine him to be this bright
16800	high-school student, and he says, "Why does the government have this
16900	foregn policy?"  So he sits there at his console and it displays for
17000	him the rationale for this foreign policy.  And he says, "Well, wouldn't
17100	it be better if they did so-and-so rather than that?" and he concocts a
17200	what seems to him proof that it would indeed be better if they did so-and-
17300	so, according to a specified criterion of what better means, which has
17400	been specified in this fantasy.  Lo and behold, he does succeed--most
17500	high school students don't succeed, but this one does succeed--in proving
17600	that it would be better if they did it differently, and the next morning
17700	when the official in charge of this policy arrives at his console, he
17800	discovers that somebody has found an improvement in the policy which has
17900	been proved to be better.  Now, this seems a bit fantastic, and in a
18000	sense, the more you know about what's going on at present  for proving
18100	programs correct, the more fantasy you can see in this, because there
18200	are some major issues which have not yet been tackled or even understood
18300	as being issues.  Let me mention a couple of them that I can see, things
18400	that we would have to be able to do in order to actually deal with
18500	policies.
18600	
18700		The first one is of course that what the policy was supposed to
18800	optimize would have to be out in the open, and this isn't the case at
18900	present with any policy, because policies are a certain kind of compromise
19000	which depend for their political viability on the fact that different groups
19100	that are affected by the policy each can do his own wishful thinking about
19200	what the policy really means.  I'd like to see that corrected.  That is,
19300	I'm a kind of a fierce rationalist, having recently become much fiercer,
19400	and prove that one should go so far as that one should politically decide,
19500	that is that the public should politically decide, on what it is that is
19600	to be optimized, and then we should go ahead and optimize it.  Of course,
19700	we could lose our shirts on some bungle in this process, but there is
19800	some circle mechanisms where it would turn out that, no, that wasn't really
19900	what we wanted to optimize.
20000	
20100		Aside from that, there are a couple of other issues.  One is that
20200	we would have to use something that I would call a pseudo-proof, where
20300	certain kinds of propositions are accepted  simply because you haven't
20400	been able to prove the contrary, or you haven't been able to find any
20500	evidence to the contrary.  But, I can give a trivial example of that, which
20600	is how will I get back to the airport tomorrow.  Will I drive this Avis
20700	car bac there?  And without any evidence to the contrary, I will assume
20800	that the Avis car is drivable tomorrow.  So in a sense you could perhaps
20900	hope to prove that my strategy for gettting back to the airport is correct
21000	but it would sort of be modulo this kind of assumption and I don't want to
21100	go into the technical problems of this, this may seem easy to you but in
21200	fact there are some rather substantial technical problems involved in this
21300	kind of thing.  The other thing is that if we were ever going to deal with
21400	any kind of policies we would have to be able to deal with partial
21500	information of all kinds, that is, that's where at present programming
21600	is a nice area in which to work.  The computer is completely described,
21700	at least we understand about not taking into account and proving the
21800	program correct the possible breakdowns of the computer, and things are
21900	in a very clear-cut area.  Whereas in many areas where other kinds of
22000	systems that one might want to prove correct, all the information is not
22100	present and you have to prove some things on the basis of partial
22200	information.  Well, I went immediately from a programming example to an
22300	extreme kind of example of proving things correct in order to show what
22400	an extremist I am, but let me remind you that there are some intermediate
22500	examples like the example of some kind of physical systems, like the
22600	computer itself, that one would like to prove correct, like systems involving
22700	hardware.  One could think of some kind of space travel system and so forth
22800	that could benefit from a computer check proof that all contingencies of
22900	some kind had been accounted for.
23000	
23100		Now, these seem to be the ultimate goals and therefore sort of
23200	suitable for an after-dinner speech.  Let me mention something, this is
23300	a kind of digression, I'm not sure I'll get back to the main topic or not.
23400	Something that has come up and that I want to complain about.  And it
23500	may seem a little bit quixotic to complain about this, but this has to do
23600	with commercial secrecy in this field, and in some other purely scientific
23700	fields.  I will say what triggered this off.  It's specifically a grumble
23800	about IBM.  But two IBM people today came up to me on separate occassions
23900	about 15 minutes apart, and each of them told me that he had something
24000	that I would be interested in, and I presume that it was in this field,
24100	and that it was company-confidential, and that he might be able to say
24200	something about it later.  I didn't say anything to the first one, and
24300	I'm afraid I was unnecessarily rude to the second one.  And one can
24400	understand their bureaucratic problem which I would like to call to your
24500	attention.  The bureaucratic problem which they face, or at least their
24600	doctrine of what they seem to think they face, is that well, they're not
24700	allowed to preannounce computers because they've been accused of being
24800	unfair about that and telling people that, if you just hold up buying that
24900	CDC computer we'll have a great computer for you shortly, and so they're
25000	not supposed to do that, and so  this extends now to where, well, it has
25100	extended ever since my first contact with IBM which was in 1955, to,
25200	well, everything is secret unless it is told to be otherwise.  Now, that
25300	is an exaggeration, and one can find out things if one wants to.  The
25400	bigger shot you are the more you can find out, and people are
25500	individually reasonable, but nevertheless there's a lot that goes on there
25600	and of course in other companies as well which is objectionally kept
25700	secret.  Now, I'd like to mention to make this concrete with regard to
25800	some things of my own interest.  The first thing which should I think
25900	offend other people in this room, which was company-confidential for a
26000	while, was the Vienna definition language.  I ran across some reports of
26100	this, or I guess I was told about some reports and they sent them to me
26200	because after all at the time I was an IBM consultant so they could send
26300	them to me, but I was really sort of offended by this being company-
26400	confidential because as it turned out it was based on abstract syntax
26500	which was something that I was quite proud of having introduced and I
26600	was offended at the publicity of this coming out later rather than sooner.
26700	I wrote some nasty letters about that.  Anyway, that was one thing about
26800	something that turned up in this area which was, I would say, kept
26900	secret, and for, as far as one could see, for no reason whatsoever, since 
27000	it certainly wasn't a part of any product then and it hasn't become a
27100	part of any product as far as one could see in the 6 or 7 years since the
27200	matter was raised.  It was simply that it took them that long to
27300	disentangle their  bureaucracy and decide to -------(?) it.  Maybe an
27400	indignant letter may have helped there.  
27500	
27600		Another matter which came up in this connection  was LISP;
27700	namely, IBM has made at various time some improvements in LISP and
27800	also made a big symbolic population system for algebraic calculation
27900	based on LISP and this one was company-confidential for a while.  Well,
28000	the question  is, is there anything that anybody could do about this
28100	rather than just to grumble at them, and I consider that just to grumble
28200	at them is being constructive, but I would like to be even more
28300	constructive and to help IBM make a larger contribution to computer
28400	science and I would like to suggest that the ACM help IBM make a
28500	larger contribution to computer science, in the first place, by taking
28600	the matter up with them officially, and bickering with them about it,
28700	but in order to pursuade the lawyers that it is better to be reasonable
28800	in this area than not, one has to have a threat.  And I thought of two
28900	of them.
29000	
29100		The first of them is that one should consider that a symposium
29200	like this one should require a non-secrecy pledge or statement for
29300	attendance.  What is says is not that the individual wishing to attend
29400	will tell everything he knows about everything (that seems a little
29500	unreasonable) but in the area of the conference itself, that he does
29600	not have any secrets that he is obliged to keep.  I think that people
29700	who found it not possible to sign such a statement would of course be
29800	slightly inconvenienced, because the proceedings would be out after a
29900	while, and they could find out what they needed to know eventually from
30000	people who had been able to sign such a statement, but nevertheless they
30100	wouldn't get to come to so many meetings in nice places like this, and
30200	they might try a little harder to pursuade their company to be reasonable
30300	in such matters.
30400	
30500		The other one concerns the anti-trust which is that the anti-trust
30600	decisions, that is the consent decree and so forth, has always
30700	been interpreted in such a way as to encourage secrecy, whereas I
30800	think the ACM should point out to the Justice Department that really the
30900	field would be more advanced, competition might even be increased, if
31000	these matters were interpreted in such a way as to discourage secrecy.
31100	For example, there are all the eager fellows who would like to make
31200	compatible disc drives as soon as they can find out the interface
31300	specification.  Well, I hope that no one will take offense at my
31400	desire to help IBM and others increase their contribution to computer
31500	science.
31600